$\forall$$T$:Type, $X$:MaInterface($T$), ${\it es}$:ES, $e$:E. ma{-}in{-}interface(${\it es}$;$X$;$e$) $\in$ $\mathbb{B}$